w:World, e'':E. FairFifo  rcv?(e'')  match(link(e'');time(sender(e''));time(e'')) 

latex

Definitions

b, lnk(k), rcv(l,tg), t  T, {T}, P  Q, x:A. B(x), SQType(T), Knd, s = t, Prop, s ~ t, False, A, P & Q, AB, i  j < k, , {x:A| B(x) }, {i..j}, left+right, #$n, , x:AB(x), x:A. B(x), x:AB(x), True, isrcv(k), FairFifo, tag(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), ecase1(e;info;i.f(i);l,e'.g(l;e')), sender(e), sender(e), w-info(w;e), link(e), rcv?(e), E, World, time(e), match(l;t;t'), x.A(x), kind(e)

Lemmas

world wf, w-E wf, w-ekind wf, false wf, true wf, fair-fifo wf, mu-property, nat wf, w-match-exists, le wf, assert wf, w-match wf, w-time wf, Knd wf, Knd sq